\begin{tabbing}
1. $a$ : $\mathbb{N}$
\\[0ex]2. $b$ : $\mathbb{N}$
\\[0ex]$\vdash$  \{\=$m$:$\mathbb{N}\mid$ \+
\\[0ex]$\forall$$k$:$\mathbb{N}$.
\\[0ex]($a$ = fib($k$))
\\[0ex]$\Rightarrow$ (($k$ $\leq$ 0) $\Rightarrow$ ($b$ = 0))
\\[0ex]$\Rightarrow$ ((0 $<$ $k$) $\Rightarrow$ ($b$ = fib($k$ {-} 1)))
\\[0ex]$\Rightarrow$ ($m$ = fib(0+$k$))\} 
\-
\end{tabbing}